A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a). SqStable(f  g) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), x(s), x. t(x), a:A fp B(a), P  Q, f  g, SqStable(P), b, f(x), False, , A c B, True, , Top, A, b, P & Q, P  Q, Unit, x  dom(f), T
Lemmas	squash wf, sq stable all, decidable assert, sq stable implies, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, bool wf, true wf, sq stable and, decidable false, sq stable equal, false wf, fpf-ap wf, sq stable from decidable, fpf wf, deq wf